plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)
== i, j:ff.C.
== owes_ack(i,j) initially@i  = ff & awaiting(i,j) initially@i  = ff
== & (e:E.
== & (([e: i is_req j]  ((awaiting(i,j) when e) = ff))
== & (& ([e: i is_ack j]  ((awaiting(i,j) after e) = ff))
== & (& ([e: i is_req j]  ((awaiting(i,j) after e) = tt))
== & (& ((loc(e) = i & (((awaiting(i,j) after e) = (awaiting(i,j) when e))))
== & (& ( ([e: i is_ack j]  [e: i is_req j]))
== & (& ([e: i is_ack j]  ((owes_ack(i,j) when e) = tt))
== & (& ([e: i is_req j]  ((owes_ack(i,j) after e) = tt))
== & (& ([e: i is_ack j]  ((owes_ack(i,j) after e) = ff))
== & (& ((loc(e) = i & (((owes_ack(i,j) after e) = (owes_ack(i,j) when e))))
== & (& ( ([e: i is_req j]  [e: i is_ack j]))
== & (& (((loc(e) = i) c ((owes_ack(i,j) after e) = tt))
== & (& ( (e':E. ((e < e') & [e': i is_ack j])))) 

latex

---

clarification:

plus-ify{i:l}
plus-ify(es; ff; is_req; is_ack; awaiting; owes_ack)
== i:ff.C, j:ff.C.
== es-initially(es;i;owes_ack(i,j)) = ff   & es-initially(es;i;awaiting(i,j)) = ff  
== & (e:es-E(es).
== & ((snd-it(ff;is_req;e;i;j)  (es-when(es; (awaiting(i,j)); e) = ff  ))
== & (& (rcv-it(ff;is_ack;e;i;j)  (es-after(es; (awaiting(i,j)); e) = ff  ))
== & (& (snd-it(ff;is_req;e;i;j)  (es-after(es; (awaiting(i,j)); e) = tt  ))
== & (& ((es-loc(es; e) = i  Id
== & (& (& ((es-after(es; (awaiting(i,j)); e) = es-when(es; (awaiting(i,j)); e)  )))
== & (& ( (rcv-it(ff;is_ack;e;i;j)  snd-it(ff;is_req;e;i;j)))
== & (& (snd-it(ff;is_ack;e;i;j)  (es-when(es; (owes_ack(i,j)); e) = tt  ))
== & (& (rcv-it(ff;is_req;e;i;j)  (es-after(es; (owes_ack(i,j)); e) = tt  ))
== & (& (snd-it(ff;is_ack;e;i;j)  (es-after(es; (owes_ack(i,j)); e) = ff  ))
== & (& ((es-loc(es; e) = i  Id
== & (& (& ((es-after(es; (owes_ack(i,j)); e) = es-when(es; (owes_ack(i,j)); e)  )))
== & (& ( (rcv-it(ff;is_req;e;i;j)  snd-it(ff;is_ack;e;i;j)))
== & (& (((es-loc(es; e) = i  Id) c (es-after(es; (owes_ack(i,j)); e) = tt  ))
== & (& ( (e':es-E(es). (es-causl(es; e; e') & snd-it(ff;is_ack;e';i;j))))) 

latex

Definitions	ff.C, x initially@i , x:A. B(x), ff, A, x when e, P  Q, [e: i p j], P  Q, A c B, Id, loc(e), s = t, , (x after e), f(a), tt, x:A. B(x), E, P & Q, (e < e'), [e: i p j]
FDL editor aliases	plus-ify